* Step 1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [4] x1 + [1] x2 + [0]
p(cons) = [1] x2 + [1]
p(eq) = [0]
p(false) = [2]
p(if) = [5] x1 + [1] x2 + [1] x3 + [5]
p(ifinter) = [1] x1 + [1] x3 + [1] x4 + [0]
p(ifmem) = [1] x1 + [0]
p(inter) = [1] x1 + [1] x2 + [3]
p(mem) = [2]
p(nil) = [2]
p(s) = [1] x1 + [0]
p(true) = [2]
Following rules are strictly oriented:
app(cons(x,l1),l2) = [4] l1 + [1] l2 + [4]
> [4] l1 + [1] l2 + [1]
= cons(x,app(l1,l2))
app(nil(),l) = [1] l + [8]
> [1] l + [0]
= l
if(false(),x,y) = [1] x + [1] y + [15]
> [1] y + [0]
= y
if(true(),x,y) = [1] x + [1] y + [15]
> [1] x + [0]
= x
inter(l1,cons(x,l2)) = [1] l1 + [1] l2 + [4]
> [1] l1 + [1] l2 + [2]
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = [1] x + [5]
> [2]
= nil()
inter(cons(x,l1),l2) = [1] l1 + [1] l2 + [4]
> [1] l1 + [1] l2 + [2]
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = [1] x + [5]
> [2]
= nil()
mem(x,cons(y,l)) = [2]
> [0]
= ifmem(eq(x,y),x,l)
Following rules are (at-least) weakly oriented:
eq(0(),0()) = [0]
>= [2]
= true()
eq(0(),s(x)) = [0]
>= [2]
= false()
eq(s(x),0()) = [0]
>= [2]
= false()
eq(s(x),s(y)) = [0]
>= [0]
= eq(x,y)
ifinter(false(),x,l1,l2) = [1] l1 + [1] l2 + [2]
>= [1] l1 + [1] l2 + [3]
= inter(l1,l2)
ifinter(true(),x,l1,l2) = [1] l1 + [1] l2 + [2]
>= [1] l1 + [1] l2 + [4]
= cons(x,inter(l1,l2))
ifmem(false(),x,l) = [2]
>= [2]
= mem(x,l)
ifmem(true(),x,l) = [2]
>= [2]
= true()
mem(x,nil()) = [2]
>= [2]
= false()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
mem(x,nil()) -> false()
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
if(false(),x,y) -> y
if(true(),x,y) -> x
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [4] x1 + [1] x2 + [3]
p(cons) = [1] x2 + [1]
p(eq) = [1]
p(false) = [5]
p(if) = [2] x2 + [1] x3 + [1]
p(ifinter) = [1] x1 + [0]
p(ifmem) = [1] x1 + [3]
p(inter) = [6]
p(mem) = [6]
p(nil) = [0]
p(s) = [1]
p(true) = [1]
Following rules are strictly oriented:
ifmem(false(),x,l) = [8]
> [6]
= mem(x,l)
ifmem(true(),x,l) = [4]
> [1]
= true()
mem(x,nil()) = [6]
> [5]
= false()
Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) = [4] l1 + [1] l2 + [7]
>= [4] l1 + [1] l2 + [4]
= cons(x,app(l1,l2))
app(nil(),l) = [1] l + [3]
>= [1] l + [0]
= l
eq(0(),0()) = [1]
>= [1]
= true()
eq(0(),s(x)) = [1]
>= [5]
= false()
eq(s(x),0()) = [1]
>= [5]
= false()
eq(s(x),s(y)) = [1]
>= [1]
= eq(x,y)
if(false(),x,y) = [2] x + [1] y + [1]
>= [1] y + [0]
= y
if(true(),x,y) = [2] x + [1] y + [1]
>= [1] x + [0]
= x
ifinter(false(),x,l1,l2) = [5]
>= [6]
= inter(l1,l2)
ifinter(true(),x,l1,l2) = [1]
>= [7]
= cons(x,inter(l1,l2))
inter(l1,cons(x,l2)) = [6]
>= [6]
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = [6]
>= [0]
= nil()
inter(cons(x,l1),l2) = [6]
>= [6]
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = [6]
>= [0]
= nil()
mem(x,cons(y,l)) = [6]
>= [4]
= ifmem(eq(x,y),x,l)
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
if(false(),x,y) -> y
if(true(),x,y) -> x
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [5] x1 + [4] x2 + [4]
p(cons) = [1] x1 + [1] x2 + [2]
p(eq) = [0]
p(false) = [1]
p(if) = [2] x1 + [4] x2 + [2] x3 + [0]
p(ifinter) = [1] x1 + [3] x2 + [4] x3 + [4] x4 + [0]
p(ifmem) = [1] x1 + [1]
p(inter) = [4] x1 + [4] x2 + [0]
p(mem) = [1]
p(nil) = [1]
p(s) = [1] x1 + [2]
p(true) = [1]
Following rules are strictly oriented:
ifinter(false(),x,l1,l2) = [4] l1 + [4] l2 + [3] x + [1]
> [4] l1 + [4] l2 + [0]
= inter(l1,l2)
Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) = [5] l1 + [4] l2 + [5] x + [14]
>= [5] l1 + [4] l2 + [1] x + [6]
= cons(x,app(l1,l2))
app(nil(),l) = [4] l + [9]
>= [1] l + [0]
= l
eq(0(),0()) = [0]
>= [1]
= true()
eq(0(),s(x)) = [0]
>= [1]
= false()
eq(s(x),0()) = [0]
>= [1]
= false()
eq(s(x),s(y)) = [0]
>= [0]
= eq(x,y)
if(false(),x,y) = [4] x + [2] y + [2]
>= [1] y + [0]
= y
if(true(),x,y) = [4] x + [2] y + [2]
>= [1] x + [0]
= x
ifinter(true(),x,l1,l2) = [4] l1 + [4] l2 + [3] x + [1]
>= [4] l1 + [4] l2 + [1] x + [2]
= cons(x,inter(l1,l2))
ifmem(false(),x,l) = [2]
>= [1]
= mem(x,l)
ifmem(true(),x,l) = [2]
>= [1]
= true()
inter(l1,cons(x,l2)) = [4] l1 + [4] l2 + [4] x + [8]
>= [4] l1 + [4] l2 + [3] x + [1]
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = [4] x + [4]
>= [1]
= nil()
inter(cons(x,l1),l2) = [4] l1 + [4] l2 + [4] x + [8]
>= [4] l1 + [4] l2 + [3] x + [1]
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = [4] x + [4]
>= [1]
= nil()
mem(x,cons(y,l)) = [1]
>= [1]
= ifmem(eq(x,y),x,l)
mem(x,nil()) = [1]
>= [1]
= false()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [0]
p(app) = [1] x2 + [4]
p(cons) = [1] x2 + [0]
p(eq) = [1]
p(false) = [2]
p(if) = [4] x1 + [1] x2 + [1] x3 + [0]
p(ifinter) = [1] x1 + [3]
p(ifmem) = [1] x1 + [1]
p(inter) = [5]
p(mem) = [2]
p(nil) = [5]
p(s) = [1] x1 + [0]
p(true) = [0]
Following rules are strictly oriented:
eq(0(),0()) = [1]
> [0]
= true()
Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) = [1] l2 + [4]
>= [1] l2 + [4]
= cons(x,app(l1,l2))
app(nil(),l) = [1] l + [4]
>= [1] l + [0]
= l
eq(0(),s(x)) = [1]
>= [2]
= false()
eq(s(x),0()) = [1]
>= [2]
= false()
eq(s(x),s(y)) = [1]
>= [1]
= eq(x,y)
if(false(),x,y) = [1] x + [1] y + [8]
>= [1] y + [0]
= y
if(true(),x,y) = [1] x + [1] y + [0]
>= [1] x + [0]
= x
ifinter(false(),x,l1,l2) = [5]
>= [5]
= inter(l1,l2)
ifinter(true(),x,l1,l2) = [3]
>= [5]
= cons(x,inter(l1,l2))
ifmem(false(),x,l) = [3]
>= [2]
= mem(x,l)
ifmem(true(),x,l) = [1]
>= [0]
= true()
inter(l1,cons(x,l2)) = [5]
>= [5]
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = [5]
>= [5]
= nil()
inter(cons(x,l1),l2) = [5]
>= [5]
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = [5]
>= [5]
= nil()
mem(x,cons(y,l)) = [2]
>= [2]
= ifmem(eq(x,y),x,l)
mem(x,nil()) = [2]
>= [2]
= false()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(app) = [5] x1 + [1] x2 + [2]
p(cons) = [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(if) = [4] x1 + [4] x2 + [4] x3 + [2]
p(ifinter) = [1] x1 + [4] x3 + [4] x4 + [5]
p(ifmem) = [1] x1 + [0]
p(inter) = [4] x1 + [4] x2 + [0]
p(mem) = [0]
p(nil) = [2]
p(s) = [0]
p(true) = [0]
Following rules are strictly oriented:
ifinter(true(),x,l1,l2) = [4] l1 + [4] l2 + [5]
> [4] l1 + [4] l2 + [2]
= cons(x,inter(l1,l2))
Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) = [5] l1 + [1] l2 + [12]
>= [5] l1 + [1] l2 + [4]
= cons(x,app(l1,l2))
app(nil(),l) = [1] l + [12]
>= [1] l + [0]
= l
eq(0(),0()) = [0]
>= [0]
= true()
eq(0(),s(x)) = [0]
>= [0]
= false()
eq(s(x),0()) = [0]
>= [0]
= false()
eq(s(x),s(y)) = [0]
>= [0]
= eq(x,y)
if(false(),x,y) = [4] x + [4] y + [2]
>= [1] y + [0]
= y
if(true(),x,y) = [4] x + [4] y + [2]
>= [1] x + [0]
= x
ifinter(false(),x,l1,l2) = [4] l1 + [4] l2 + [5]
>= [4] l1 + [4] l2 + [0]
= inter(l1,l2)
ifmem(false(),x,l) = [0]
>= [0]
= mem(x,l)
ifmem(true(),x,l) = [0]
>= [0]
= true()
inter(l1,cons(x,l2)) = [4] l1 + [4] l2 + [8]
>= [4] l1 + [4] l2 + [5]
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = [4] x + [8]
>= [2]
= nil()
inter(cons(x,l1),l2) = [4] l1 + [4] l2 + [8]
>= [4] l1 + [4] l2 + [5]
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = [4] x + [8]
>= [2]
= nil()
mem(x,cons(y,l)) = [0]
>= [0]
= ifmem(eq(x,y),x,l)
mem(x,nil()) = [0]
>= [0]
= false()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
{app,eq,if,ifinter,ifmem,inter,mem}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 2 + 2*x1 + x2
p(cons) = x1 + x2
p(eq) = x1*x2
p(false) = 0
p(if) = x1 + 2*x1*x2 + 2*x2 + 2*x3
p(ifinter) = 3 + x1 + 2*x2 + 2*x3 + 2*x3*x4 + 2*x4
p(ifmem) = 2*x1 + 2*x2*x3
p(inter) = 3 + 2*x1 + 2*x1*x2 + 2*x2
p(mem) = 2*x1*x2
p(nil) = 0
p(s) = 1 + x1
p(true) = 0
Following rules are strictly oriented:
eq(s(x),s(y)) = 1 + x + x*y + y
> x*y
= eq(x,y)
Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) = 2 + 2*l1 + l2 + 2*x
>= 2 + 2*l1 + l2 + x
= cons(x,app(l1,l2))
app(nil(),l) = 2 + l
>= l
= l
eq(0(),0()) = 0
>= 0
= true()
eq(0(),s(x)) = 0
>= 0
= false()
eq(s(x),0()) = 0
>= 0
= false()
if(false(),x,y) = 2*x + 2*y
>= y
= y
if(true(),x,y) = 2*x + 2*y
>= x
= x
ifinter(false(),x,l1,l2) = 3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l2
= inter(l1,l2)
ifinter(true(),x,l1,l2) = 3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l2 + x
= cons(x,inter(l1,l2))
ifmem(false(),x,l) = 2*l*x
>= 2*l*x
= mem(x,l)
ifmem(true(),x,l) = 2*l*x
>= 0
= true()
inter(l1,cons(x,l2)) = 3 + 2*l1 + 2*l1*l2 + 2*l1*x + 2*l2 + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l1*x + 2*l2 + 2*x
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = 3 + 2*x
>= 0
= nil()
inter(cons(x,l1),l2) = 3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*l2*x + 2*x
>= 3 + 2*l1 + 2*l1*l2 + 2*l2 + 2*l2*x + 2*x
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = 3 + 2*x
>= 0
= nil()
mem(x,cons(y,l)) = 2*l*x + 2*x*y
>= 2*l*x + 2*x*y
= ifmem(eq(x,y),x,l)
mem(x,nil()) = 0
>= 0
= false()
* Step 7: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(cons) = {2},
uargs(ifinter) = {1},
uargs(ifmem) = {1}
Following symbols are considered usable:
{app,eq,if,ifinter,ifmem,inter,mem}
TcT has computed the following interpretation:
p(0) = 0
p(app) = 1 + 2*x1*x2 + 2*x1^2 + x2 + 2*x2^2
p(cons) = 1 + x2
p(eq) = 1
p(false) = 0
p(if) = 2 + 2*x2 + x2*x3 + x3
p(ifinter) = x1 + 2*x3*x4
p(ifmem) = x1 + x3
p(inter) = 2*x1*x2
p(mem) = x2
p(nil) = 0
p(s) = 0
p(true) = 1
Following rules are strictly oriented:
eq(0(),s(x)) = 1
> 0
= false()
eq(s(x),0()) = 1
> 0
= false()
Following rules are (at-least) weakly oriented:
app(cons(x,l1),l2) = 3 + 4*l1 + 2*l1*l2 + 2*l1^2 + 3*l2 + 2*l2^2
>= 2 + 2*l1*l2 + 2*l1^2 + l2 + 2*l2^2
= cons(x,app(l1,l2))
app(nil(),l) = 1 + l + 2*l^2
>= l
= l
eq(0(),0()) = 1
>= 1
= true()
eq(s(x),s(y)) = 1
>= 1
= eq(x,y)
if(false(),x,y) = 2 + 2*x + x*y + y
>= y
= y
if(true(),x,y) = 2 + 2*x + x*y + y
>= x
= x
ifinter(false(),x,l1,l2) = 2*l1*l2
>= 2*l1*l2
= inter(l1,l2)
ifinter(true(),x,l1,l2) = 1 + 2*l1*l2
>= 1 + 2*l1*l2
= cons(x,inter(l1,l2))
ifmem(false(),x,l) = l
>= l
= mem(x,l)
ifmem(true(),x,l) = 1 + l
>= 1
= true()
inter(l1,cons(x,l2)) = 2*l1 + 2*l1*l2
>= l1 + 2*l1*l2
= ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) = 0
>= 0
= nil()
inter(cons(x,l1),l2) = 2*l1*l2 + 2*l2
>= 2*l1*l2 + l2
= ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) = 0
>= 0
= nil()
mem(x,cons(y,l)) = 1 + l
>= 1 + l
= ifmem(eq(x,y),x,l)
mem(x,nil()) = 0
>= 0
= false()
* Step 8: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
app(nil(),l) -> l
eq(0(),0()) -> true()
eq(0(),s(x)) -> false()
eq(s(x),0()) -> false()
eq(s(x),s(y)) -> eq(x,y)
if(false(),x,y) -> y
if(true(),x,y) -> x
ifinter(false(),x,l1,l2) -> inter(l1,l2)
ifinter(true(),x,l1,l2) -> cons(x,inter(l1,l2))
ifmem(false(),x,l) -> mem(x,l)
ifmem(true(),x,l) -> true()
inter(l1,cons(x,l2)) -> ifinter(mem(x,l1),x,l2,l1)
inter(x,nil()) -> nil()
inter(cons(x,l1),l2) -> ifinter(mem(x,l2),x,l1,l2)
inter(nil(),x) -> nil()
mem(x,cons(y,l)) -> ifmem(eq(x,y),x,l)
mem(x,nil()) -> false()
- Signature:
{app/2,eq/2,if/3,ifinter/4,ifmem/3,inter/2,mem/2} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,eq,if,ifinter,ifmem,inter,mem} and constructors {0
,cons,false,nil,s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))